#include "PDTNumConst.h"
#include "PDTCodeGraph.h"
#include "PDTZ3GraphVisitor.h"

PDTNumConst::PDTNumConst(PDTCodeGraph & CG) :
  PDTExpNumSing(CG)
{
    nValue = this;
  CG.addConst(this);
}

PDTNumConstInt::PDTNumConstInt(PDTCodeGraph & CG, long long value) :
  PDTNumConst(CG) 
{
  this->value = value;
}

Z3_ast
PDTNumConstInt::Z3NodeVisit (PDTZ3Visitor &ZV)
{
  if (Z3node != NULL)
    return Z3node;

  Z3node = Z3_mk_int(ZV.ctx, this->value, ZV.Int);
  return Z3node;
}

PDTNumConstDbl::PDTNumConstDbl(PDTCodeGraph & CG, double value) :
  PDTNumConst(CG)
{
  this->value = value;
}

Z3_ast
PDTNumConstDbl::Z3NodeVisit (PDTZ3Visitor &ZV)
{
  if (Z3node != NULL)
    return Z3node;

  Z3node = Z3_mk_int(ZV.ctx, (int) this->value, ZV.Int);//TODO: change ZV.Int to be ZV.double
  //Z3node = Z3_mk_int(ZV.ctx,  this->value, ZV.Dbl);
  return Z3node;
}

